Nuprl Lemma : atom-free-es-Msg
0,22
postcript
pdf
es
:ES. AtomFree(Type;Msg)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
Void
,
S
T
,
S
T
,
f
(
a
)
,
x
:
A
B
(
x
)
,
x
.
A
(
x
)
,
Msg(
M
)
,
P
&
Q
,
es-M(
es
)
,
Msg
,
ES
,
Type
,
Id
,
x
:
A
B
(
x
)
,
IdLnk
,
AtomFree(
T
;
x
)
Lemmas
event
system
wf
,
IdLnk
wf
,
atom-free-IdLnk
,
Id
wf
,
atom-free-Id
origin
es:ES. AtomFree(Type;Msg) es:ES. AtomFree(Type;Msg) 
Tx:A. B(x)
T
T
B(x)
x.A(x)
B(x)